$\forall$$T$:Type, ${\it eq}$, ${\it leq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$).
\\[0ex]IsEqFun($T$;${\it eq}$) $\Rightarrow$ Linorder($T$;$a$,$b$.$\uparrow$($a$ ${\it leq}$ $b$)) $\Rightarrow$ (mk\_oset($T$;${\it eq}$;${\it leq}$) $\in$ LOSet)